a, b:IdLnk. Dec(a = b) 

latex

Definitions	x. t(x), P  Q, P & Q, P  Q, P  Q, a = b, t  T, Prop, IdLnk, Dec(P), b, x:A. B(x)
Lemmas	decidable assert, assert wf, eq lnk wf, decidable wf, IdLnk wf, assert-eq-lnk, decidable functionality, all functionality wrt iff